{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE RecordWildCards  #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TupleSections    #-}

-- | This module contains (most of) the code needed to lift Haskell entitites,
--   . code- (CoreBind), and data- (Tycon) definitions into the spec level.

module Language.Haskell.Liquid.Bare.Measure
  ( makeHaskellMeasures
  , makeHaskellInlines
  , makeHaskellDataDecls
  , makeMeasureSelectors
  , makeMeasureSpec
  , makeMeasureSpec'
  , makeOpaqueReflMeasures
  , getReflDCs
  , varMeasures
  , getMeasVars
  , makeClassMeasureSpec
  -- , makeHaskellBounds
  , varLocSym
  ) where

import qualified Control.Exception as Ex
import Prelude hiding (mapM, error)
import Data.Bifunctor
import qualified Data.Maybe as Mb
import Text.PrettyPrint.HughesPJ (text)
-- import Text.Printf     (printf)

import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S

import           Language.Fixpoint.SortCheck (isFirstOrder)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Transforms.CoreToLogic
import qualified Language.Fixpoint.Misc                as Misc
import qualified Language.Haskell.Liquid.Misc          as Misc
import           Language.Haskell.Liquid.Misc             ((.||.))
import qualified Liquid.GHC.API       as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc      as GM
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import qualified Language.Haskell.Liquid.Types.RefType as RT
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
-- import           Language.Haskell.Liquid.Types.Bounds
import qualified Language.Haskell.Liquid.Measure       as Ms

import qualified Language.Haskell.Liquid.Bare.Types    as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve  as Bare
import qualified Language.Haskell.Liquid.Bare.Expand   as Bare
import qualified Language.Haskell.Liquid.Bare.DataType as Bare
import qualified Language.Haskell.Liquid.Bare.ToBare   as Bare
import           Language.Haskell.Liquid.UX.Config
import Control.Monad (mapM)
import qualified Data.List as L

import GHC.Base (Int(I#))

--------------------------------------------------------------------------------
makeHaskellMeasures :: Config -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
                    -> [Measure (Located BareType) (Located LHName)]
--------------------------------------------------------------------------------
makeHaskellMeasures cfg src tycEnv lmap spec
          = Bare.measureToBare <$> ms
  where
    ms    = makeMeasureDefinition cfg tycEnv lmap cbs <$> mSyms
    cbs   = Ghc.flattenBinds (_giCbs src)
    mSyms = S.toList (Ms.hmeas spec)

makeMeasureDefinition
  :: Config -> Bare.TycEnv -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName
  -> Measure LocSpecType Ghc.DataCon
makeMeasureDefinition cfg tycEnv lmap cbs x =
  case L.find ((x ==) . makeGHCLHNameLocatedFromId . fst) cbs of
    Nothing ->
      Ex.throw $
        errHMeas x "Cannot extract measure from haskell function"
    Just (v, cexp) -> Ms.mkM vx vinfo mdef MsLifted (makeUnSorted allowTC (Ghc.varType v) mdef)
                     where
                       vx           = reflectLHName (Ghc.nameModule $ Ghc.getName v) <$> x
                       mdef         = coreToDef' cfg tycEnv lmap vx v cexp
                       vinfo        = GM.varLocInfo (logicType allowTC) v

    where allowTC = typeclass cfg

makeUnSorted :: Bool -> Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
makeUnSorted allowTC ty defs
  | isMeasureType ta
  = mempty
  | otherwise
  = map defToUnSortedExpr defs
  where
    ta = go $ Ghc.expandTypeSynonyms ty

    go (Ghc.ForAllTy _ t) = go t
    go Ghc.FunTy{ Ghc.ft_arg = p, Ghc.ft_res = t} | isErasable p = go t
    go Ghc.FunTy{ Ghc.ft_arg = t } = t
    go t                  = t -- this should never happen!

    isMeasureType (Ghc.TyConApp _ ts) = all Ghc.isTyVarTy ts
    isMeasureType _                   = False

    defToUnSortedExpr defn =
      (xx:(fst <$> binds defn),
       Ms.bodyPred (F.eApps (F.EVar $ lhNameToResolvedSymbol $ F.val $ measure defn) [F.expr xx]) (body defn))

    xx = F.vv $ Just 10000
    isErasable = if allowTC then GM.isEmbeddedDictType else Ghc.isClassPred

coreToDef' :: Config -> Bare.TycEnv -> LogicMap -> Located LHName -> Ghc.Var -> Ghc.CoreExpr
           -> [Def LocSpecType Ghc.DataCon]
coreToDef' cfg tycEnv lmap vx v defn =
  case runToLogic embs lmap dm cfg (errHMeas vx) (coreToDef vx v defn) of
    Right l -> l
    Left e  -> Ex.throw e
  where
    embs    = Bare.tcEmbs       tycEnv
    dm      = Bare.tcDataConMap tycEnv

errHMeas :: Located LHName -> String -> Error
errHMeas x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)

--------------------------------------------------------------------------------
makeHaskellInlines :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
                   -> [(LocSymbol, LMap)]
--------------------------------------------------------------------------------
makeHaskellInlines cfg src embs lmap spec
         = makeMeasureInline cfg embs lmap cbs <$> inls
  where
    cbs  = Ghc.flattenBinds (_giCbs src)
    inls = S.toList        (Ms.inlines spec)

makeMeasureInline
  :: Config -> F.TCEmb Ghc.TyCon -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName
  -> (LocSymbol, LMap)
makeMeasureInline cfg embs lmap cbs x =
  case L.find ((val x ==) . makeGHCLHNameFromId . fst) cbs of
    Nothing        -> Ex.throw $ errHMeas x "Cannot inline haskell function"
    Just (v, defn) -> (vx, coreToFun' cfg embs Nothing lmap vx v defn ok)
                     where
                       vx         = F.atLoc x (F.symbol v)
                       ok (xs, e) = LMap vx (F.symbol <$> xs) (either id id e)

-- | @coreToFun'@ takes a @Maybe DataConMap@: we need a proper map when lifting
--   measures and reflects (which have case-of, and hence, need the projection symbols),
--   but NOT when lifting inlines (which do not have case-of).
--   For details, see [NOTE:Lifting-Stages]

coreToFun' :: Config -> F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
           -> (([Ghc.Var], Either F.Expr F.Expr) -> a) -> a
coreToFun' cfg embs dmMb lmap x v defn ok = either Ex.throw ok act
  where
    act  = runToLogic embs lmap dm cfg err xFun
    xFun = coreToFun x v defn
    err  str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)
    dm   = Mb.fromMaybe mempty dmMb


-------------------------------------------------------------------------------
makeHaskellDataDecls :: Config -> Ms.BareSpec -> [Ghc.TyCon]
                     -> [DataDecl]
--------------------------------------------------------------------------------
makeHaskellDataDecls cfg spec tcs
  | exactDCFlag cfg = Bare.dataDeclSize spec
                    . Mb.mapMaybe tyConDataDecl
                    -- . F.tracepp "makeHaskellDataDecls-3"
                    . zipMap   (hasDataDecl spec . fst)
                    -- . F.tracepp "makeHaskellDataDecls-2"
                    . liftableTyCons
                    -- . F.tracepp "makeHaskellDataDecls-1"
                    . filter isReflectableTyCon
                    $ tcs
  | otherwise       = []


isReflectableTyCon :: Ghc.TyCon -> Bool
isReflectableTyCon  = Ghc.isFamInstTyCon .||. Ghc.isVanillaAlgTyCon

liftableTyCons :: [Ghc.TyCon] -> [(Ghc.TyCon, DataName)]
liftableTyCons
  = F.notracepp "LiftableTCs 3"
  . zipMapMaybe tyConDataName
  . F.notracepp "LiftableTCs 2"
  . filter   (not . Ghc.isBoxedTupleTyCon)
  . F.notracepp "LiftableTCs 1"
  -- . (`sortDiff` wiredInTyCons)
  -- . F.tracepp "LiftableTCs 0"

zipMap :: (a -> b) -> [a] -> [(a, b)]
zipMap f xs = zip xs (map f xs)

zipMapMaybe :: (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe f = Mb.mapMaybe (\x -> (x, ) <$> f x)

hasDataDecl :: Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
hasDataDecl spec
                 = \tc -> F.notracepp (msg tc) $ M.lookupDefault defn (tyConDataName tc) decls
  where
    msg tc       = "hasDataDecl " ++ show (tyConDataName tc)
    defn         = NoDecl Nothing
    decls        = M.fromList [ (Just dn, hasDecl d)
                                | d     <- Ms.dataDecls spec
                                , let dn = tycName d]

{-tyConDataDecl :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-}
tyConDataDecl :: ((Ghc.TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl (_, HasDecl)
  = Nothing
tyConDataDecl ((tc, dn), NoDecl szF)
  = Just $ DataDecl
      { tycName   = dn
      , tycTyVars = F.symbol <$> GM.tyConTyVarsDef tc
      , tycPVars  = []
      , tycDCons  = Just (decls tc)
      , tycSrcPos = GM.getSourcePos tc
      , tycSFun   = szF
      , tycPropTy = Nothing
      , tycKind   = DataReflected
      }
      where decls = map dataConDecl . Ghc.tyConDataCons

tyConDataName :: Ghc.TyCon -> Maybe DataName
tyConDataName tc
  | vanillaTc  = Just $ DnName $ makeGHCLHNameLocated tc
  | d:_ <- dcs = Just $ DnCon $ makeGHCLHNameLocated d
  | otherwise  = Nothing
  where
    vanillaTc  = Ghc.isVanillaAlgTyCon tc
    dcs        = Misc.sortOn F.symbol (Ghc.tyConDataCons tc)

dataConDecl :: Ghc.DataCon -> DataCtor
dataConDecl d     = {- F.notracepp msg $ -} DataCtor dx (F.symbol <$> as) [] xts outT
  where
    isGadt        = not (Ghc.isVanillaDataCon d)
    -- msg           = printf "dataConDecl (gadt = %s)" (show isGadt)
    xts           = [(makeGeneratedLogicLHName $ Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
    dx            = makeGHCLHNameLocated d
    its           = zip [1..] ts
    (as,_ps,ts,ty)  = Ghc.dataConSig d
    outT          = Just (RT.bareOfType ty :: BareType)
    _outT :: Maybe BareType
    _outT
      | isGadt    = Just (RT.bareOfType ty)
      | otherwise = Nothing





--------------------------------------------------------------------------------
-- | 'makeMeasureSelectors' converts the 'DataCon's and creates the measures for
--   the selectors and checkers that then enable reflection.
--------------------------------------------------------------------------------

makeMeasureSelectors :: Config -> Bare.DataConMap -> Located DataConP -> [Measure SpecType Ghc.DataCon]
makeMeasureSelectors cfg dm (Loc l l' c)
  = Misc.condNull (exactDCFlag cfg) (checker : Mb.mapMaybe go' fields) --  internal measures, needed for reflection
 ++ Misc.condNull autofields (Mb.mapMaybe go fields) --  user-visible measures.
  where
    dc         = dcpCon    c
    isGadt     = dcpIsGadt c
    xts        = dcpTyArgs c
    autofields = not isGadt
    go ((x, t), i)
      -- do not make selectors for functional fields
      | isFunTy t && not (higherOrderFlag cfg)
      = Nothing
      | otherwise
        -- TODO: Use as origin module the module where the measure is created
      = Just $ makeMeasureSelector (Loc l l' x) (projT i) dc n i

    go' ((_,t), i)
      -- do not make selectors for functional fields
      | isFunTy t && not (higherOrderFlag cfg)
      = Nothing
      | otherwise
      = Just $ makeMeasureSelector (Loc l l' (makeGeneratedLogicLHName $ Bare.makeDataConSelector (Just dm) dc i)) (projT i) dc n i

    fields   = zip (reverse xts) [1..]
    n        = length xts
    checker  = makeMeasureChecker (Loc l l' (makeGeneratedLogicLHName $ Bare.makeDataConChecker dc)) checkT dc n
    projT i  = dataConSel permitTC dc n (Proj i)
    checkT   = dataConSel permitTC dc n Check
    permitTC = typeclass cfg

dataConSel :: Bool -> Ghc.DataCon -> Int -> DataConSel -> SpecType
dataConSel permitTC dc n Check    = mkArrow (map (, mempty) as) [] [xt] bareBool
  where
    (as, _, xt)          = {- traceShow ("dataConSel: " ++ show dc) $ -} bkDataCon permitTC dc n

dataConSel permitTC dc n (Proj i) = mkArrow (map (, mempty) as) [] [xt] (mempty <$> ti)
  where
    ti                   = Mb.fromMaybe err $ Misc.getNth (i-1) ts
    (as, ts, xt)         = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} bkDataCon permitTC dc n
    err                  = panic Nothing $ "DataCon " ++ show dc ++ "does not have " ++ show i ++ " fields"

-- bkDataCon :: DataCon -> Int -> ([RTVar RTyVar RSort], [SpecType], (Symbol, SpecType, RReft))
bkDataCon :: (Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) => Bool -> Ghc.DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (F.Symbol, RFInfo, RRType r, r))
bkDataCon permitTC dcn nFlds  = (as, ts, (F.dummySymbol, classRFInfo permitTC, t, mempty))
  where
    ts                = RT.ofType <$> Misc.takeLast nFlds (map Ghc.irrelevantMult _ts)
    t                 = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $
                          RT.ofType  $ Ghc.mkTyConApp tc tArgs'
    as                = makeRTVar . RT.rTyVar <$> (αs ++ αs')
    ((αs,αs',_,_,_ts,_t), _t0) = hammer dcn
    tArgs'            = take (nArgs - nVars) tArgs ++ (Ghc.mkTyVarTy <$> αs)
    nVars             = length αs
    nArgs             = length tArgs
    (tc, tArgs)       = Mb.fromMaybe err (Ghc.splitTyConApp_maybe _t)
    err               = GM.namedPanic dcn ("Cannot split result type of DataCon " ++ show dcn)
    hammer dc         = (Ghc.dataConFullSig dc, Ghc.varType . Ghc.dataConWorkId $ dc)

data DataConSel = Check | Proj Int

bareBool :: SpecType
bareBool = RApp (RTyCon Ghc.boolTyCon [] defaultTyConInfo) [] [] mempty


{- | NOTE:Use DataconWorkId

      dcWorkId :: forall a1 ... aN. (a1 ~ X1 ...) => T1 -> ... -> Tn -> T
      checkT   :: forall as. T -> Bool
      projT t  :: forall as. T -> t

-}

makeMeasureSelector :: (Show a1) => Located LHName -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
makeMeasureSelector x s dc n i = M { msName = x, msSort = s, msEqns = [eqn], msKind = MsSelector, msUnSorted = mempty}
  where
    eqn                        = Def x dc Nothing args (E (F.EVar $ mkx i))
    args                       = (, Nothing) . mkx <$> [1 .. n]
    mkx j                      = F.symbol ("xx" ++ show j)

makeMeasureChecker :: Located LHName -> SpecType -> Ghc.DataCon -> Int -> Measure SpecType Ghc.DataCon
makeMeasureChecker x s0 dc n = M { msName = x, msSort = s, msEqns = eqn : (eqns <$> filter (/= dc) dcs), msKind = MsChecker, msUnSorted = mempty }
  where
    s       = F.notracepp ("makeMeasureChecker: " ++ show x) s0
    eqn     = Def x dc Nothing ((, Nothing) . mkx <$> [1 .. n])       (P F.PTrue)
    eqns d  = Def x d  Nothing ((, Nothing) . mkx <$> [1 .. nArgs d]) (P F.PFalse)
    nArgs d = length (Ghc.dataConOrigArgTys d)
    mkx j   = F.symbol ("xx" ++ show j)
    dcs     = Ghc.tyConDataCons (Ghc.dataConTyCon dc)


----------------------------------------------------------------------------------------------
makeMeasureSpec' :: Bool -> MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(Located LHName, RRType F.Reft)])
----------------------------------------------------------------------------------------------
makeMeasureSpec' allowTC mspec0 = (ctorTys, measTys)
  where
    ctorTys             = fmap RT.uRType <$> ctorTys0
    (ctorTys0, measTys) = Ms.dataConTypes allowTC mspec
    mspec               = first (mapReft ur_reft) mspec0

----------------------------------------------------------------------------------------------
makeMeasureSpec :: Bare.Env -> Bare.SigEnv -> ModName -> (ModName, Ms.BareSpec) ->
                   Bare.Lookup (Ms.MSpec SpecType Ghc.DataCon)
----------------------------------------------------------------------------------------------
makeMeasureSpec env sigEnv myName (name, spec)
  = mkMeasureDCon env
  . mkMeasureSort env
  . first val
  . bareMSpec     env sigEnv myName name
  $ spec

--- Returns all the reflected symbols.
--- If Env is provided, the symbols are qualified using the environment.
getLocReflects :: Bare.ModSpecs -> S.HashSet F.Symbol
getLocReflects = S.unions . map names . M.elems
  where
    names modSpec = unqualified modSpec
    unqualified modSpec = S.unions
      [ S.map (lhNameToResolvedSymbol . val) (Ms.reflects modSpec)
      , S.map val $ Ms.privateReflects modSpec
      , S.fromList (lhNameToResolvedSymbol . val . snd <$> Ms.asmReflectSigs modSpec)
      , S.fromList (lhNameToResolvedSymbol . val . fst <$> Ms.asmReflectSigs modSpec)
      , S.map (lhNameToResolvedSymbol . val) (Ms.inlines modSpec)
      , S.map (lhNameToResolvedSymbol . val) (Ms.hmeas modSpec)
      ]

-- Get all the symbols that are defined in the logic, based on the environment and the specs.
getDefinedSymbolsInLogic :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs -> S.HashSet F.Symbol
getDefinedSymbolsInLogic env measEnv specs =
  S.unions (uncurry getFromAxioms <$> specsList) -- reflections that ended up in equations
    `S.union` getLocReflects specs -- reflected symbols
    `S.union` measVars -- Get the data constructors, ex. for Lit00.0
    `S.union` S.unions (getDataDecls . snd <$> specsList) -- get the Predicated type defs, ex. for T1669.CSemigroup
    `S.union` S.unions (getAliases . snd <$> specsList) -- aliases, ex. for T1738Lib.incr
  where
    specsList = M.toList specs
    getFromAxioms _modName spec = S.fromList $
      F.eqName <$> Ms.axeqs spec
    measVars     = S.fromList $ fst <$> getMeasVars env measEnv
    getDataDecls spec = S.unions $
      getFromDataCtor <$>
        concat (tycDCons `Mb.mapMaybe` (dataDecls spec ++ newtyDecls spec))
    getFromDataCtor decl = S.fromList $
      map lhNameToResolvedSymbol $ val (dcName decl) : (fst <$> dcFields decl)
    getAliases spec = S.fromList $ lhNameToUnqualifiedSymbol . val . rtName <$> Ms.ealiases spec

-- Get the set of `DataCon`s (DCs) needed for the reflection of a given list of variables,
-- and which are not already present in the logic
getReflDCs :: Bare.MeasEnv -> [Ghc.Var] -> S.HashSet Ghc.DataCon
getReflDCs measEnv vars = dcsUndefinedInLogic
  where
    -- List of wired DCs that cannot be found in the measure environment as they are
    -- eliminated in the translation from core.
    -- Written as a list of symbols because that's easier than trying to get the corresponding DCs from GHC.
    wired = S.fromList $ F.symbol <$> [show 'True, show 'False, show 'I#]
    notWired dc = not $ GM.qualifiedNameSymbol (Ghc.getName dc) `S.member` wired
    -- Undefined ones are those that are not already defined in the measure environement and are not wired
    dcsUndefinedInLogic = S.filter notWired $ allDCInUnfoldings `S.difference` definedDCs
    -- Get the defined DataCons from the measure environement
    definedDCs = S.fromList $ (GM.idDataConM . fst) `Mb.mapMaybe` Bare.meDataCons measEnv
    allDCInUnfoldings = getDCsOfUnfoldingOfVars vars

----------------------------------------------------
-- Looks at the given list of equations and finds any undefined symbol in the logic,
-- for which we need to introduce an opaque reflection.
-- Returns the corresponding measures. Second part of the returned tuple is the information to save
-- to the `meOpaqueRefl` field of the measure environment.
makeOpaqueReflMeasures :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs ->
              [(Ghc.Var, LocSpecType, F.Equation)] ->
              ([MSpec SpecType Ghc.DataCon], [(Ghc.Var, Measure LocBareType ctor)])
makeOpaqueReflMeasures env measEnv specs eqs =
  unzip $ createMeasureForVar <$> S.toList (varsUndefinedInLogic `S.union` requestedOpaqueRefl)
  where
    thisModule = Ghc.tcg_mod (Bare.reTcGblEnv env)
    -- Get the set of variables for the requested opaque reflections
    requestedOpaqueRefl = S.unions
      . map (S.map getVar . Ms.opaqueReflects . snd)
      . M.toList $ specs
    getVar sym = case Bare.lookupGhcIdLHName env sym of
      Right x -> x
      Left _ -> panic (Just $ GM.fSrcSpan sym) "function to reflect not in scope"
    definedSymbols = getDefinedSymbolsInLogic env measEnv specs
    undefinedInLogic v = not (S.member (F.symbol v) definedSymbols)
    -- Variables to consider
    varsUndefinedInLogic = S.unions $
      S.filter undefinedInLogic .
      (\(v, _, eq) -> getFreeVarsOfReflectionOfVar v eq) <$> eqs
    -- Main function: creates a (dummy) measure about a given variable
    createMeasureForVar :: Ghc.Var -> (MSpec SpecType Ghc.DataCon, (Ghc.Var, Measure LocBareType ctor))
    createMeasureForVar var =
      (Ms.mkMSpec' [smeas], (var, bmeas))
      where
        locSym = F.atLoc (loc specType) (reflectLHName thisModule $ makeGHCLHNameFromId var)
        specType = varSpecType var
        bareType = varBareType var
        bmeas = M locSym bareType [] MsReflect []
        smeas = M locSym (val specType) [] MsReflect []

getUnfoldingOfVar :: Ghc.Var -> Maybe Ghc.CoreExpr
getUnfoldingOfVar = getExpr . Ghc.realUnfoldingInfo . Ghc.idInfo
  where
    getExpr :: Ghc.Unfolding -> Maybe Ghc.CoreExpr
    getExpr (Ghc.CoreUnfolding expr _ _ _ _) = Just expr
    getExpr _ = Nothing

-- Get the set of "free" symbols in the (reflection of the) unfolding of a given variable.
-- Free symbols are those that are not already in the logic and that appear in
-- the reflection of the unfolding.
-- For this purpose, you need to give the variable naming the definition to reflect
-- and its corresponding equation in the logic.
getFreeVarsOfReflectionOfVar  :: Ghc.Var -> F.Equation -> S.HashSet Ghc.Var
getFreeVarsOfReflectionOfVar var eq =
    S.filter (\v -> F.symbol v `S.member` freeSymbolsInReflectedBody) freeVarsInCoreExpr
  where
    reflExpr = getUnfoldingOfVar var
    getAllFreeVars = Ghc.exprSomeFreeVarsList (const True)
    freeVarsInCoreExpr = maybe S.empty (S.fromList . getAllFreeVars) reflExpr
    freeSymbolsInReflectedBody = F.exprSymbolsSet (F.eqBody eq)

-- Collect all the DataCon that appear in the unfolding of a given variable.
getDCsOfUnfoldingOfVars :: [Ghc.Var] -> S.HashSet Ghc.DataCon
getDCsOfUnfoldingOfVars vars = S.unions $ collectDataCons <$> getUnfoldingOfVar `Mb.mapMaybe` vars

-- Collect all DataCon that occur in case split alternatives of an expression
collectDataCons :: Ghc.CoreExpr -> S.HashSet Ghc.DataCon
collectDataCons expr = go expr S.empty
  where
    go (Ghc.Var _) acc = acc
    go (Ghc.Lit _) acc = acc
    go (Ghc.App f e) acc = go f (go e acc)
    go (Ghc.Lam _ e) acc = go e acc
    go (Ghc.Let bind e) acc = go e (goBind bind acc)
    go (Ghc.Case e _ _ alts) acc = foldr goAlt (go e acc) alts
    go (Ghc.Cast e _) acc = go e acc
    go (Ghc.Tick _ e) acc = go e acc
    go (Ghc.Type _) acc = acc
    go (Ghc.Coercion _) acc = acc

    -- Special auxiliary function for `Alt` which is precisely where we get the datacons
    goAlt (Ghc.Alt (Ghc.DataAlt dc) _ e) acc = S.insert dc (go e acc)
    goAlt (Ghc.Alt _ _ e) acc = go e acc

    goBind (Ghc.NonRec _ e) acc = go e acc
    goBind (Ghc.Rec binds) acc = foldr (go . snd) acc binds

bareMSpec :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> Ms.BareSpec -> Ms.MSpec LocBareType (Located LHName)
bareMSpec env sigEnv myName name spec = Ms.mkMSpec ms cms ims oms
  where
    cms        = F.notracepp "CMS" $ filter inScope $             Ms.cmeasures spec
    ms         = F.notracepp "UMS" $ filter inScope $ expMeas <$> Ms.measures  spec
    ims        = F.notracepp "IMS" $ filter inScope $ expMeas <$> Ms.imeasures spec
    oms        = F.notracepp "OMS" $ filter inScope $ expMeas <$> Ms.omeasures spec
    expMeas    = expandMeasure rtEnv
    rtEnv      = Bare.sigRTEnv          sigEnv
    force      = name == myName
    inScope z = F.notracepp ("inScope1: " ++ F.showpp (msName z)) (force ||  okSort z)
    okSort     = Bare.knownGhcType env . msSort

mkMeasureDCon :: Bare.Env -> Ms.MSpec t (F.Located LHName) -> Bare.Lookup (Ms.MSpec t Ghc.DataCon)
mkMeasureDCon env m = do
  let ns = measureCtors m
  dcs   <- mapM (Bare.lookupGhcDataConLHName env) ns
  return $ mkMeasureDCon_ m (zip (val <$> ns) dcs)

-- mkMeasureDCon env name m = mkMeasureDCon_ m [ (val n, symDC n) | n <- measureCtors m ]
--   where
--     symDC                = Bare.lookupGhcDataCon env name "measure-datacon"

mkMeasureDCon_ :: Ms.MSpec t (F.Located LHName) -> [(LHName, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon_ m ndcs = fmap (tx . val) m
  where
    tx                = Misc.mlookup (M.fromList ndcs)

measureCtors ::  Ms.MSpec t (F.Located LHName) -> [F.Located LHName]
measureCtors = Misc.sortNub . fmap ctor . concat . M.elems . Ms.ctorMap

mkMeasureSort :: Bare.Env -> Ms.MSpec BareType (F.Located LHName)
              -> Ms.MSpec SpecType (F.Located LHName)
mkMeasureSort env (Ms.MSpec c mm cm im) =
  Ms.MSpec (map txDef <$> c) (tx <$> mm) (tx <$> cm) (tx <$> im)
    where
      ofMeaSort :: F.SourcePos -> BareType -> SpecType
      ofMeaSort l = Bare.ofBareType env l Nothing

      tx :: Measure BareType ctor -> Measure SpecType ctor
      tx (M n s eqs k u) = M n (ofMeaSort l s) (txDef <$> eqs) k u where l = GM.fSourcePos n

      txDef :: Def BareType ctor -> Def SpecType ctor
      txDef d = first (ofMeaSort l) d                              where l = GM.fSourcePos (measure d)



--------------------------------------------------------------------------------
-- | Expand Measures -----------------------------------------------------------
--------------------------------------------------------------------------------
-- type BareMeasure = Measure LocBareType LocSymbol

expandMeasure :: BareRTEnv -> BareMeasure -> BareMeasure
expandMeasure rtEnv m = m
  { msSort = RT.generalize <$> msSort m
  , msEqns = expandMeasureDef rtEnv <$> msEqns m
  }

expandMeasureDef :: BareRTEnv -> Def t (Located LHName) -> Def t (Located LHName)
expandMeasureDef rtEnv d = d
  { body  = F.notracepp msg $ Bare.expand rtEnv l (body d) }
  where
    l     = loc (measure d)
    bs    = fst <$> binds d
    msg   = "QUALIFY-EXPAND-BODY" ++ F.showpp (bs, body d)

------------------------------------------------------------------------------
varMeasures :: (Monoid r) => Bare.Env -> [(F.Symbol, Located (RRType r))]
------------------------------------------------------------------------------
varMeasures env =
  [ (F.symbol v, varSpecType v)
      | v <- Bare.reDataConIds env
      , GM.isDataConId v
      , isSimpleType (Ghc.varType v) ]

getMeasVars :: Bare.Env -> Bare.MeasEnv -> [(F.Symbol, Located (RRType F.Reft))]
getMeasVars env measEnv = Bare.meSyms measEnv -- ms'
                            ++ Bare.meClassSyms measEnv -- cms'
                            ++ varMeasures env

varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)
varSpecType = fmap (RT.ofType . Ghc.varType) . GM.locNamedThing

varBareType :: (Monoid r) => Ghc.Var -> Located (BRType r)
varBareType = fmap (RT.bareOfType . Ghc.varType) . GM.locNamedThing

varLocSym :: Ghc.Var -> LocSymbol
varLocSym v = F.symbol <$> GM.locNamedThing v

isSimpleType :: Ghc.Type -> Bool
isSimpleType = isFirstOrder . RT.typeSort mempty

makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t
                     -> [(Located LHName, CMeasure (RType c tv r2))]
makeClassMeasureSpec Ms.MSpec{..} = tx <$> M.elems cmeasMap
  where
    tx (M n s _ _ _) = (n, CM n (mapReft ur_reft s))


{-
expandMeasureBody :: Bare.Env -> ModName -> BareRTEnv -> SourcePos -> Body -> Body
expandMeasureBody env name rtEnv l (P   p) = P   (Bare.expandQualify env name rtEnv l p)
expandMeasureBody env name rtEnv l (R x p) = R x (Bare.expandQualify env name rtEnv l p)
expandMeasureBody env name rtEnv l (E   e) = E   (Bare.expandQualify env name rtEnv l e)


makeHaskellBounds :: F.TCEmb TyCon -> CoreProgram -> S.HashSet (Var, LocSymbol) -> BareM RBEnv  -- TODO-REBARE
makeHaskellBounds embs cbs xs = do
  lmap <- gets logicEnv
  M.fromList <$> mapM (makeHaskellBound embs lmap cbs) (S.toList xs)

makeHaskellBound :: F.TCEmb TyCon
                 -> LogicMap
                 -> [Bind Var]
                 -> (Var, Located Symbol)
                 -> BareM (LocSymbol, RBound)
makeHaskellBound embs lmap  cbs (v, x) =
  case filter ((v  `elem`) . GM.binders) cbs of
    (NonRec v def:_)   -> toBound v x <$> coreToFun' embs lmap x v def return
    (Rec [(v, def)]:_) -> toBound v x <$> coreToFun' embs lmap x v def return
    _                  -> throwError $ errHMeas x "Cannot make bound of haskell function"



toBound :: Var -> LocSymbol -> ([Var], Either F.Expr F.Expr) -> (LocSymbol, RBound)
toBound v x (vs, Left p) = (x', Bound x' fvs ps xs p)
  where
    x'         = capitalizeBound x
    (ps', xs') = L.partition (hasBoolResult . varType) vs
    (ps , xs)  = (txp <$> ps', txx <$> xs')
    txp v      = (dummyLoc $ simpleSymbolVar v, RT.ofType $ varType v)
    txx v      = (dummyLoc $ symbol v,          RT.ofType $ varType v)
    fvs        = (((`RVar` mempty) . RTV) <$> fst (splitForAllTyCoVars $ varType v)) :: [RSort]

toBound v x (vs, Right e) = toBound v x (vs, Left e)

capitalizeBound :: Located Symbol -> Located Symbol
capitalizeBound = fmap (symbol . toUpperHead . symbolString)
  where
    toUpperHead []     = []
    toUpperHead (x:xs) = toUpper x:xs

-}

